﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using System.Diagnostics.Contracts;
using SimpleIR;

namespace PInfoModel
{
	/// <summary>
	/// This class maintains info we want to preserve for a single program point (bytecode)
	/// </summary>
	public sealed class ProgramPointInfo
	{
		/// <summary>
		/// The abstract model representing the program state before executing the statement.
		/// </summary>
		public PIModel PreOperationModel;

		/// <summary>
		/// The abstract model representing the program state after executing the statement.
		/// </summary>
		public PIModel PostOperationModel;

		public ProgramPointInfo(PIModel prem, PIModel postm)
		{
			this.PreOperationModel = prem;
			this.PostOperationModel = postm;
		}

		internal void Serialize(PInfoSerializer sr)
		{
			sr.WriteStartTag("ProgPointInfo");

			sr.WriteBool("URPost", this.PostOperationModel == null);

			if(this.PostOperationModel != null)
				this.PostOperationModel.Serialize(sr);

			sr.WriteEndTag("ProgPointInfo");
		}

		internal static ProgramPointInfo Deserialize(PInfoDeSerializer dsr)
		{
			dsr.ReadStartTag("ProgPointInfo");

			bool urpost = dsr.ReadBool("URPost");

			PIModel postm = null;
			if(!urpost)
				postm = PIModel.Deserialize(dsr);

			dsr.ReadEndTag("ProgPointInfo");

			return new ProgramPointInfo(null, postm);
		}
	}
}

